|
In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea.〔 Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system. ==Overview== A logical framework is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities. To describe a logical framework, one must provide the following: # A characterization of the class of object-logics to be represented; # An appropriate meta-language; # A characterization of the mechanism by which object-logics are represented. This is summarized by: :''‘Framework = Language + Representation’''. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Logical framework」の詳細全文を読む スポンサード リンク
|